* add some implementation for the "norm" method in FloatDomain, however at the moment incorrect

Now, the norm method is called at eval_binop and successfully fails,
which currently is wanted like this, just to test that it works.
We need to change it now s.t. it prints a warning instead of an error.

* Rework norm slightly s.t. it uses set_overflow_flag now, which however is still incorrect

* Add FloatMessage message category in messageCategory.ml

Also add it in options.schema.json

* Add a todo note for later in sarifRules.ml

* Add a regression test for float that expects a warning for division by zeron / infinity

* Clean up floatDomain.ml slightly: Remove TODOs/FIXMEs and inline message warning

* Fix regression test naming and merge them together

* Remove FloatMessage module in messageCategory.ml, as it's not needed anymore

* Remove todo message

* Remove todo message

* Remove todo comments and/or clean up some stuff

* Clean up float domain etc. with fixes from PR

- Better warning message
- use is_top function instead of checking for None in the domain
- revert unrelated change
- make 'warn.float' option not a default option
- make regression test as minimal as possible

* In floatDomain.ml, rearrange of_const function s.t. it finds the norm function

* Add float warning parameter to 03-infinity_or_nan.c regression test

)

- lattice related functions (leq, widen, narrow, join, meet)
 - arithmetic operations (add, sub, mul, div)
 - casts (f2i, i2f)

* Support FFloat and FDouble
- Implement float operators in C
- Support FFloat and FDouble

* Allow using DBL_MIN, DBL_MAX
Some compilers specifiy DBL_MIN, DBL_MAX as long double.
As we do not support long double in neither cil nor goblint itself, but want to use DBL_MIN, DBL_MAX, we have no other option than to explicitly check for this two cases

* Find another location where get_ikind results in an error
* Further refine determining safe casts with floats

Merge remote

Co-authored-by: Julian Erhard <[email protected]>